Logic bậc nhất - còn được gọi là logic vị từ (predicate logic), quantificational logic, và phép tính vị từ bậc nhất (first-order predicate calculus) là một tập hợp các hệ thống hình thức được sử dụng trong toán học, triết học, ngôn ngữ học và khoa học máy tính. Logic bậc nhất sử dụng các biến lượng từ hóa trên các đối tượng phi logic và cho phép sử dụng các câu có chứa các biến, do đó, thay vì các mệnh đề như Socrates là một người đàn ông, có thể có các biểu thức dạng "tồn tại x sao cho x là Socrates và x là một người đàn ông", và "tồn tại" là một lượng từ trong khi x là một biến.[1] Điều này phân biệt nó với logic mệnh đề, không sử dụng các lượng từ hay các quan hệ;[2] theo nghĩa này, logic mệnh đề là nền tảng của logic bậc nhất.Một lý thuyết về một chủ đề thường là một logic bậc nhất cùng với một miền diễn ngôn được chỉ định trong đó các biến lượng hóa được khởi tạo, các hàm từ miền vào chính nó, một số hữu hạn các vị từ xác định trên miền đó và một tập hợp các tiên đề được tin là đúng cho những đối tượng trong miền diễn ngôn. (Đôi khi "lý thuyết" cũng được hiểu theo nghĩa hình thức hơn, là một tập hợp các câu trong logic bậc nhất.)Cụm từ "bậc nhất" phân biệt logic bậc nhất với logic bậc cao hơn trong đó có các vị từ có các đối số là các vị từ khác hoặc các hàm.[3] :56 Trong các lý thuyết bậc nhất, các vị từ thường được liên kết với các tập hợp. Trong các lý thuyết bậc cao được diễn giải, các vị từ có thể được hiểu là tập hợp của các tập hợp.